basic
\\[0ex]RelsIso($T$;${\it T'}$;$x$,$y$.$R$($x$;$y$);$x$,$y$.${\it R'}$($x$;$y$);$f$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$x$:$T$, $y$:$T$. $R$($x$;$y$) $\Leftarrow\!\Rightarrow$ ${\it R'}$($f$($x$);$f$($y$))